操作系统微内核架构研究

微内核是操作系统内核的一种，在工控系统、嵌入式系统、实时系统等领域发挥着重要作用。本文较为全面地研究了微内核技术的各个方面，包括微内核的定义、微内核的体系架构、微内核的发展历史、微内核的特点、微内核的应用场景，以及作者所进行的部分研究工作。本文部分内容和图来自网上，由于内容较多，有些没有标注，如果原作者觉得不合适请联系删除。

在计算机科学中，内核是操作系统的核心部分，它管理着系统的各种资源，譬如时钟、中断、存储、进程、设备驱动、原语等。应用程序运行在内核之上，并通过系统调用访问内核空间。

从内核架构来划分，操作系统内核可分为微内核(Micro Kernel)和宏内核(Monolithic Kernel，也翻译为单内核)。如下图所示，微内核操作系统仅在内核中保留了调度、基础IPC、虚拟内存管理等少数核心功能模块，它们位于内核空间，而操作系统的其他功能模块（譬如文件系统、驱动程序等）与用户应用程序一起运行于用户空间；宏内核操作系统在内核中包括了整个操作系统的大部分功能模块（譬如文件系统、驱动程序等），并且这些系统模块都运行在同一个内核地址空间，模块之间通过简单的系统调用进行协调工作。

微内核（通常缩写为μ内核）由一群数量尽可能最少的软件程序组成，它们负责提供实现一个操作系统所必须的各种机制。这些机制就是之前提到的线程/进程调度机制、基础的进程间通信机制（IPC）、虚拟内存管理机制等；而包括文件系统、驱动程序在内的其他各种功能模块都放到用户空间。微内核的最小化也称为Jochen Liedtke最小化原则。Jochen Liedtke是一名德国科学家。这里区分两个术语，操作系统微内核即指微内核，微内核操作系统则指一种基于微内核架构的操作系统。

                                         图1 微内核与宏内核架构

从操作系统功能模块来看，操作系统厂商依据自己的实际情况，可以将宏内核操作系统中的部分功能模块从内核空间移到用户空间，也可以将微内核操作系统中的部分功能模块从用户空间移到内核空间，由此就构成了微内核、小内核、大内核、宏内核等称谓。对于介于微内核和宏内核之间的小内核、大内核来说，有时也把它们称之为混合内核。对于操作系统厂商来说，没有必要严格遵守微内核的最小化原则，非要做一个严格意义上的微内核，或者完全意义上的宏内核。本文在后面主要讨论微内核和宏内核。

在图1的微内核架构中，按照官方说法，位于用户空间的各个功能模块被设计成一个个功能独立的服务器（Server），由微内核采用消息通信机制来调度各个服务器完成工作。为避免混淆，这里的服务器可以理解为一个服务器程序。微内核相当于客户端程序（Client）。

从理论上来说，基于消息通信的两个程序（Client和Server）可以位于同一台机器，也可以位于不同机器。因而，微内核操作系统中的这些服务器可以是分布式的，它们可能位于同一台机器，也可能位于其他机器。这里再次强调，只是理论上是这样，真正这样实现的操作系统还极少。

微内核的分布式架构是有意义的。从下面链接可知，鸿蒙操作系统声称自己具有两个特点：微内核、分布式。采用分布式消息通信机制，可以实现鸿蒙操作系统与各类硬件设备（例如手机、平板、手表、PC等）的互联。这种消息通信机制也被说成为分布式总线。

（参见：鸿蒙系统：微内核，分布式_华为）

                                        图2 基于分布式总线的鸿蒙操作系统的万物互联机制

在图1的微内核架构中，各个服务器程序相互独立，也有个别人把这种架构称之为“插件架构”。

如下图所示（微内核架构 - 简书），在软件开发领域，插件化架构由一个中间的核心系统和若干插件模块组成。该架构最大的优势是允许第三方开发者遵循一定的开发规范添加额外的插件化应用。采用插件架构的软件有很多，例如Eclipse、企业ERP软件等，这类软件自身具备丰富功能，同时支持第三方应用的即插即用；并且第三方插件化程序的安装、运行、卸载以及故障不会对原有系统造成任何影响。

                                        图3 软件插件架构

在插件架构中，核心系统的功能稳定，很少变更。它只拥有能使应用运行的最小功能逻辑(例如插件模块的注册、加载、卸载，以及插件模块之间的相互通信等)不涉及任何特定业务；插件系统具备良好的扩展性，可根据特定业务需求而变更其业务逻辑。 插件架构本质上是将一个软件系统中的变化部分封装在插件中，从而实现不同业务之间的隔离性，达到系统快速灵活扩展的目的，同时所有特定业务相关逻辑的变更不会影响整体系统的稳定性。

另外，插件架构需要解决好三方面的问题：插件管理、插件链接和插件通信。

由上可知，理论上的微内核确实是一种基于插件架构的操作系统内核。

微内核的起源可以追溯到丹麦计算机先驱Per Brinch Hansen和他在丹麦计算机公司Regnecentralen任职期间的工作。当时，他领导了RC 4000计算机的软件研发。1967年，Regnecentralen正在普瓦伊的一家波兰化肥厂安装RC 4000原型机。这台计算机使用了一个小型的专门为工厂量身打造的实时操作系统。Brinch Hansen和他的团队开始关注RC 4000操作系统缺乏通用性和可重用性。他们担心每次在其他公司安装一台新机器都需要开发不同的操作系统，1969年，最终完成了RC 4000多道程序设计系统。它的内核提供了基于消息传递的进程间通信，最多可以为23个非特权进程提供进程间通信，其中每次有8个进程相互保护。

继Brinch Hansen的工作之后，自20世纪70年代以来，人们开始开发微内核，但“微内核”这个术语大概在1981年之前才首次出现。最早的操作系统内核一直都是宏内核，不过早期的宏内核操作系统因为功能过于简单而更像一个微内核操作系统。随着计算机技术的发展，新的设备驱动程序、协议栈、文件系统和其他低级系统不断出现导致宏内核一直处在开发过程中，因此需要为管理这些代码花费大量的时间。由此，微内核提出了一个新理念：所有这些新出现的服务都要像其他程序一样作为用户空间程序来实现，允许它们像任何其他程序一样单独工作、启动和停止。这不仅可以让这些服务更容易操作，而且还可以分离内核代码，使其能够进行微调，而不必担心意外的副作用。采用这种方式，操作系统的内核部分就不会频繁修改，进而便于维护和管理。

在20世纪80年代，当第一个可用的局域网出现时，微内核是一个非常热门的话题。AmigaOS Exec内核就是一个早期的例子，它于1986年引入，并在一台在商业上相对成功的PC中得到了使用。

操作系统微内核技术起始于20世纪80年代，起初被设计用来解决传统宏内核操作系统在可维护性、扩展性、可靠性和稳定性方面的诸多问题。但是伴随着微内核思想的进一步发展，最终形成了一整套操作系统设计的核心理念，即操作系统微内核仅提供最简单、基本的服务，如通信功能，而操作系统的普通服务，如文件管理、设备管理、网络管理等则在微内核以外提供。

以Mach为代表，Mach微内核操作系统试图从架构上重构宏内核操作系统但是仍然能够维持原有操作系统功能的一次尝试。为此，Mach微内核研究出了一系列概念用来支撑该项目,其中较突出的有核外页管理器和用户空间设备驱动等。Mach采用的IPC（进程间通信）策略包括消息传递、RPC（远程过程调用）、同步和通知等。

然而，包括Mach或IBM的Workplace的第一代微内核的性能都不佳。对于Mach3来说，比原来的宏内核UNIX运行慢了约50%。最终大部分人倾向于认为性能低的原因是因为IPC开销过大引起的，也有提出其他原因的。

以用户程序读写文件时所涉及到的文件操作的上下文切换为例：

以L3、L4为代表，第一代微内核从概念上验证了微内核技术的可行性，但是因为性能上的原因，并未在产业界引起大规模推广，但相关学术研究不断出现。鉴于第一代微内核在性能上的劣势，Jochen Liedtke设计了高性能的第二代微内核L4。相对于第一代微内核，第二代微内核不再是传统Unix操作系统的简单重构，而是一种全新的设计，并具有较高的性能。

L4内核支持三种抽象概念：地址空间，线程和IPC。它只提供7 个系统调用，且仅有12K字节代码。进程间通信的一个基本问题是数据需要跨越不同的地址空间。大多数操作系统的解决办法是用两次数据拷贝：用户地址空间A->内核地址空间->用户地址空间B。为了实现高性能的IPC，L4的解决办法是通过暂时地址映射实现了1次拷贝：内核把数据的目的地址暂时映射到一个位于内核地址空间的通讯窗口，然后内核把数据从用户A 地址空间拷贝到通讯窗口供用户B 使用。L4还采用了许多新颖的技术来提高内核性能，例如直接地址转换、懒惰调度（Lazy Scheduling）、使用寄存器传送短消息、减少缓存及TLB Miss等。

以seL4为代表，第三代微内核更强调安全性。seL4由澳大利亚人开发，是在第二代微内核L4基础上发展起来的。L4作为第二代微内核，通过采用同步IPC技术以及使用寄存器而非内存拷贝的方式来传递消息，解决了第一代微内核的性能低、实时性差的问题；但是第二代微内核在设计时为了追求高性能，所使用的线程ID是一种全局共享静态资源，任何任务中的线程都可以通过线程ID向其他服务器线程发起服务请求，由此形成了安全上的隐患。作为第三代微内核，seL4通过一种类似对象引用的机制即Capability进行调用，任何操作系统内核对象如线程、中断、内存等都不能直接进行操作，由此解决了第二代微内核的安全隐患问题。seL4本身就是security L4的意思。

总之，微内核技术从第一代发展到了第三代。第一代微内核停留在概念层面，试图从概念上印证微内核技术的可行性；第二代微内核更关心性能，在第一代微内核的基础上印证微内核技术的可用性；第三代微内核则关注安全性。

在安全性方面，通常认为微内核操作系统比宏内核操作系统更安全。微内核之上的模块之间相对独立，单个模块崩溃后可以重启，通常不影响全局；宏内核的模块之间因为都在内核内而纠缠在一起，一个模块的崩溃容易导致整个系统的失败。宏内核不安全的核心问题在于其不符合最低授权原则POLA（Principle Of Least Authority）。其中，最大的隐患在于宏内核可不断扩张的内核模块。例如，对Linux来说，一旦进入内核，所有的代码都运行在CPU最高等级Ring 0，内核级的恶意软件可以破坏中断表、系统调用表等关键数据。然而，在微内核架构中，进程管理、文件系统、网络服务等均运行在Ring 1并且没有动态扩展，微内核的这种封闭性很好地保障了隔离性，当然这种隔离性也带来了性能开销。

另外，由于内核较小，微内核操作系统相比宏内核操作系统还具有可靠性好、可移植性好、可维护性好的特点。

从可扩展性来看，微内核操作系统只在内核部分包括功能几乎不变的核心模块，其他模块位于内核之上，便于扩展新的模块；宏内核操作系统则在内核部分包括了大部分操作系统功能模块，添加新模块会影响到其他模块，因而不便于扩展。

在工控领域，有些系统可以连续运行几个月甚至几年。可连续性是指长时间运行而不重启；当然，如果失败后应能很快恢复运行。相比宏内核，微内核因为功能少，安全性和可靠性高，因而具有更好的连续性。

宏内核操作系统因为在内核部分包括了大部分操作系统功能模块，这些模块只需要通过函数调用的方式就可以完成相互间的调用。但是，微内核操作系统的大部分功能模块在内核之外，需要通过上下文切换和地址空间（用户空间和内核空间）切换才能够完成。这样，微内核的性能通常认为比宏内核差。但即便如此，也有观点认为微内核因为其他各种优点而会在未来的PC、服务器等领域占有一席之地。

微内核与实时性没有必然联系。因为性能和实时性是两个不同的概念，所以把实时性放在性能之后来讨论。实时内核的对比对象是分时内核或非实时内核。实时内核要求系统响应的实时性，比如火箭、无人机等的操作系统就是实时的，要求对系统的各种状态做立即处理；而分时系统则对任务做分时处理，平分处理器时间，所以不具备实时性。由于一些微内核操作系统在实时性方面做了处理，因而具有较好的实时性，但宏内核操作系统也可以在实时性方面进行优化处理。

Minix和Linux是两个著名的开源操作系统，Minix于1987年发布，主要用于教学；Linux最早在1991年发布，而1.0正式版本则在1994年发布。

Minix采用微内核架构，Linux采用宏内核架构，那么这两种架构到底谁更胜一筹呢？在1992年，Minix的发明者Andrew S. Tanenbaum和Linux的创始人Linus Benedict Torvalds为此有过一段著名的争论。不过那时候，Linux才刚刚开始。看看两位大佬的争论，对我们会有所启发。（参见：https://www.cnblogs.com/wickedboy237/archive/2013/05/12/3074009.html，邮件中是Andy Tanenbaum）

Andrew主要观点：

（1）微内核架构优于宏内核架构。

（2）Linux采用宏内核架构过时了，那是一些老的操作系统采用的方法，譬如UNIX, MS-DOS, VMS, MVS, OS/360, MULTICS。这是从90年代退回到70年代的一种设计方法，就像把一个正在运行着的C程序用BASIC重写了。在1991年还写一个宏内核操作系统真是一个愚蠢的选择。

（3）宏内核唯一可称道的地方就是性能，但现在有足够的证据表明微内核系统也能够和宏内核系统跑得一样快（比如Rick Rashid 发表的对 Mach 3.0 和宏内核系统对比的论文）。

（4）微内核架构的可移植性更好，没有必要为所有的CPU都设计一个不同的宏内核。譬如不断涌现的那些Intel CPUs: 8008、8080、8086、8088、80286、80386、80486，一直到子子孙孙无穷尽。

Linus主要观点：

（1）Linux几乎在所有的领域里面都能战胜Minix。

（2）Minix并没有把微内核的能力发挥出来，并且对于真正的在内核中的多任务处理还有问题。

（3）事实是Linux可移植性比Minix好。可移植性的存在是为了那些不会编程的人。可移植性是个好东西，但只在有意义的前提下。尝试着把一个操作系统变得可移植没有必要，其实只要附带一个轻便的API就足够了（例如POSIX标准）。一个操作系统的理念是利用硬件的特点，并且把他们隐藏在一层层的高级调用中。当然这也使得内核变得不大有移植性，但它也变得更容易设计。

从1992年到2020年，世间发生了太多变化：计算机性能变得越来越好，体积越来越小；Linux变得越来越流行；计算机用户越来越年轻。由于Linux庞大的开发者和用户群体，Linux也被开发者们移植到各类CPU架构中，并没有因为可移植性而受到阻碍。

在微内核的发展过程中，出现了很多的微内核操作系统，譬如：Mach、Fiasco.OC、Pistachio OKL4 Microvisor、seL4、NOVA、P4 Pike、Minix、μC/OS-ii、ADEOS、EPOC、EKA1、EROS、Mac OS、Windows NT、Micro Empix、TI-RTOS、WarpOS、嵌入式Linux、Windows Embedded、PSOS、VxWorks、Zircon等。

从理论上来讲，一个操作系统既可以采用微内核架构，也可以采用宏内核架构，只要有开发人员愿意进行产品研发。譬如，早期的Windows NT、Mac OS等采用微内核架构，后面因为性能问题将用户空间的一部分功能移到内核空间，构成一个混合内核。Linux则采用宏内核架构。

然而随着计算机技术和操作系统的不断发展，微内核和宏内核在不同应用场景中还是存在着实际差别。

嵌入式系统具有资源相对有限、专用性强、实时性高等特点，因此应用于嵌入式系统的操作系统必须满足系统内核小、支持实时多任务、具有存储区保护功能以及可裁剪等要求。嵌入式操作系统负责嵌入式系统的全部软硬件资源的分配、任务调度，控制和协调并发活动。它必须体现其所在系统的特征，能够通过装卸某些模块来达到系统所要求的功能。

嵌入式系统的这种需求与微内核操作系统的发展需求相吻合。现代微内核相关技术仍在继续发展和不断完善中，极小化和高IPC性能这两个基本原则仍然是设计和实现决定的驱动力。

对于嵌入式系统领域，很多系统甚至没有硬盘存储，它们更多地使用微内核操作系统。

对于工控机、PC、服务器来说，因为需要操作系统完成的功能很多，处理的任务非常复杂，因而更适合使用宏内核操作系统。

如果强调实时性，完成较简单功能的工控机也可以采用微内核操作系统，譬如VxWorks等。

再次说明，从理论上讲，微内核和宏内核操作系统都可以应用于各种场景，只是目前已经研制的各种操作系统所采取的架构导致了它们在具体应用场景中有所侧重。譬如，微内核操作系统也可以运行于一些PC或服务器上。GNU HURD是一个从1990年就开始研制的微内核操作系统，运行于Mach或L4之上，目前从官网看到的最新版本为2019年开发的Debian版本。作为一个微内核操作系统，它不需要重新启动机器就可以开发和测试新的Hurd内核组件，运行自己的内核组件不会干扰其他用户，因此不需要特殊的系统特权。内核扩展的机制在设计上是安全的：不可能将一个用户的更改强加给其他用户，除非系统管理员或授权用户这样做。但是，由于开发人员很少，进展较慢，还没有达到完全成熟好用阶段。（参见GNU HURD: GNU Hurd）

在移动、物联网操作系统领域，大家一般把相关的操作系统归类为微内核操作系统，譬如应用在智能手机和平板电脑的Android、iOS等（也有人称它们为混合内核操作系统）；之前介绍的鸿蒙操作系统，采用Zircon内核的谷歌Fuchsia，这两个微内核操作系统可能在未来万物互联的物联网系统中发挥重要作用。（参见：鸿蒙系统的微内核是什么 _企业头条 - 天眼查）

总之，对于一些专用系统，主要是实时系统、嵌入式系统、物联网系统，微内核的思想更有吸引力。究其原因，主要是因为通常这些系统都不带磁盘，整个系统都必须放在EPROM中，常常受到存储空间的限制，而所需要的服务又比较单一和简单。所以，几乎所有的实时系统、嵌入式系统和物联网系统都采用微内核。当然，微内核也有缺点，将这些服务的提供都放在进程层次上，再通过进程间通信（通常是报文的传递）提供服务，势必增加系统的运行开销，降低了效率。

与微内核相对应，其他通用式系统由于所需的服务面广而量大，采用宏内核就更为合适。

seL4是一个通过形式化验证的、代码被证明是完全正确的操作系统微内核。其实，seL4不仅是一个微内核，它还是一个类似KVM的虚拟化管理程序（hypervisor），可以在它上面运行一个虚拟机。如下图所示，seL4支持在虚拟机中运行其他Linux操作系统。

                                        图4 基于seL4的虚拟化技术

实验目的：本实验是为研究如何搭建和使用seL4系统。

实验环境：在搭建seL4编译和测试环境时，选取装有《中标麒麟操作系统V7.0》操作系统的x86机器两台，一台用于编译seL4，另一台用于测试seL4。

实验步骤：

编译环境搭建步骤如下：

（a）搭建编译依赖

yum install protobuf-compiler protobuf python2-protobuf

yum install qemu-kvm libvirt libvirt-client virt-install virt-viewer

yum install centos-release-scl scl-utils-build -y

yum install devtoolset-8-toolchain -y

yum install make automake gcc gcc-c++ kernel-devel

yum install python3-devel

pip3 install --user setuptools

pip3 install --user sel4-deps

pip3 install --user camkes-deps

yum install ghc cabal-install

yum install openssl-devel

yum install qemu-system-x86

yum install nanopb

yum install -y gcc gcc-c++ make automake

yum install ninja-build

yum install python3

yum install python2

pip3 install future

pip3 install Jinja2

pip3 install tempita

pip3 install future

pip3 install templating

pip3 install six

pip3 install ply

pip3 install protobuf grpcio-tools

（b）升级cmake版本

wget https://cmake.org/files/v3.17/cmake-3.17.0.tar.gz

tar -zxvf cmake-3.17.0.tar.gz

cd cmake-3.17.0

./bootstrap --parallel=16

gmake -j 16

gmake install

（c）编译sel4源码

mkdir sel4-tutorials-manifest

cd sel4-tutorials-manifest

repo init -u https://github.com/SEL4PROJ/sel4-tutorials-manifest

repo sync

./init --plat pc99 --tut hello-world  --solution

cd hello-world_build

ninja -j 8

测试环境搭建步骤如下：

（d）修改启动项

menuentry 'sel4-hello-world' --class fedora --class gnu-linux --class gnu --class os {

    load_video

    insmod gzio

    insmod part_msdos

    insmod xfs

    set root='hd0,msdos1'

    search --no-floppy --fs-uuid --set=root b83f90f1-65b3-4db3-b19b-ef30ca140513

    echo    'Loading seL4 kernel'

    multiboot / kernel-x86_64-pc99

    echo    'Loading initial module ...'

    module  /hello-world-image-x86_64-pc99

}

（e）准备seL4内核和应用镜像

从编译环境中复制images文件夹中的kernel-x86_64-pc99和hello-world-image-x86_64-pc99文件到测试环境的/boot文件夹下

（f）重启并选择seL4启动项

重启，选择“sel4-hello-world”启动项，在串口中出现下图画面

                                        图5 Hello World测试程序输出

至此，seL4的编译环境和测试环境搭建完毕。为了进一步研究如何修改helloworld程序，可以在编译环境中对/root/sel4-tutorials-manifest/ hello-world/src/main.c文件进行修改，如下图所示：

                                        图6 新Hello World测试源码

重新回到测试环境中的/root/sel4-tutorials-manifest/hello-world_ build目录，执行ninja clean && ninja -j 8命令，命令执行成功后，把kernel-x86_64-pc99和hello-world-image-x86_64-pc99两个文件复制到测试环境中/boot目录下，重启测试机器，选择“sel4-hello-world”启动项，可以看到修改后的源码输出，如下图所示：

                                       图7 新Hello World测试效果

实验目的：为进一步研究seL4如何使用，需要研究如何在seL4系统下进行进程间通讯。

实验环境：与实验1相同。

实验步骤：

我们写了一个server端和两个client端和CMakeLists.txt文件。

server.c代码如下图所示：

                                        图8 进程间通讯server源码

client1端代码如下图所示：

                                        图9 进程间通讯client1源码

client2端源码如下图所示：

                                        图10 进程间通讯client2源码

CMakeLists.txt代码如下：

                                        图11 进程间通讯CMake文件

对上述文件执行cmake . && ninja 命令后，在把images文件夹中的kernel-x86_64-pc99和capdl-loader-image-x86_64-pc99两个文件复制到测试环境中/boot目录下，增加启动项，重启后选择新建启动项，则会在串口中发现如下图所示输出：

                                        图12 进程间测试效果

实验目的：为了测试seL4的性能，需要对ipc、irq、schedule、signal、fault、hardware、sync、page_mapping等方面进行性能测试。

实验环境：与实验1相同。

实验步骤：

使用google-benchmark测试工具库，对每一个测试项编写一个测试程序，如下图所示：

                                        图13 性能测试工程树

针对上述源码，为每一个测试源码编写CMakeLists.txt文件，执行ninja命令成功后，把images文件夹中的kernel-x86_64-pc99和sel4benchapp-image-x86_64-pc99文件复制到测试环境的/boot目录下，增加启动项，重启后选择新增加的启动项。观察串口输出，抓取输出数据起始信息如下图所示：

                                        图14 性能测试原始数据

对原始数据进行格式化处理后，显示信息如下所示：

                                        图15 性能测试结构化数据

实验目的：为研究如何在sel4上运行Linux。

实验环境：与实验1 相同。

实验步骤：

（a）准备内核

使用中标麒麟安全操作系统V7.0系统中自带内核源码，对内核进行如下修改：

CONFIG_X86_32=y

CONFIG_X86=y

CONFIG_X86_32_SMP=n

CONFIG_SMP=n

CONFIG_NOHIGHMEM=y

CONFIG_PCI_MSI=n

CONFIG_X86_UP_APIC=n

CONFIG_SUSPEND=n

CONFIG_HIBERNATION=n

CONFIG_PM=n

CONFIG_ACPI=n

CONFIG_VIRTIO=y

CONFIG_VIRTIO_PCI=y

CONFIG_VIRTIO_NET=y

（b）准备initrd

使用中标麒麟安全操作系统V7.0系统中自带initrd

（c）编写camkes文件生成虚拟机

import ;

#include

#define VM_GUEST_CMDLINE "earlyprintk=ttyS0,115200 console=tty0 console=ttyS0,115200 i8042.nokbd=y i8042.nomux=y \

i8042.noaux=y io_delay=udelay noisapnp pci=nomsi debug root=/dev/mem"

component Init0 {

    VM_INIT_DEF()

}

assembly {

    composition {

        VM_COMPOSITION_DEF()

        VM_PER_VM_COMP_DEF(0)

    }

    configuration {

        VM_CONFIGURATION_DEF()

        VM_PER_VM_CONFIG_DEF(0)

        vm0.simple_untyped23_pool = 20;

        vm0.heap_size = 0x2000000;

        vm0.guest_ram_mb = 128;

        vm0.kernel_cmdline = VM_GUEST_CMDLINE;

        vm0.kernel_image = "bzimage";

        vm0.kernel_relocs = "bzimage";

        vm0.initrd_image = "rootfs.cpio";

        vm0.iospace_domain = 0x0f;

    }

}

（d）编写CMake文件生成sel4镜像

include(${SEL4_TUTORIALS_DIR}/settings.cmake)

sel4_tutorials_regenerate_tutorial(${CMAKE_CURRENT_SOURCE_DIR})

cmake_minimum_required(VERSION 3.8.2)

project(vm-app C ASM)

include(ExternalProject)

find_package(camkes-vm REQUIRED)

include(${CAMKES_VM_SETTINGS_PATH})

camkes_x86_vm_setup_x86_vm_environment()

include(${CAMKES_VM_HELPERS_PATH})

find_package(camkes-vm-linux REQUIRED)

include(${CAMKES_VM_LINUX_HELPERS_PATH})

include(simulation)

GenerateSimulateScript()

DeclareCAmkESVM(Init0)

GetDefaultLinuxKernelFile(default_kernel_file)

GetDefaultLinuxRootfsFile(default_rootfs_file)

DecompressLinuxKernel(extract_linux_kernel decompressed_kernel ${default_kernel _file})

AddToFileServer("bzimage" ${decompressed_kernel} DEPENDS extract_linux_kernel)

AddToFileServer("rootfs.cpio" ${default_rootfs_file})

DeclareCAmkESVMRootServer(vm_tutorial.camkes)

GenerateCAmkESRootserver()

（e）测试与验证

执行ninja命令成功后，把images文件夹中的kernel-x86_64-pc99和capdl-loader-image-x86_64-pc99文件复制到测试环境的/boot目录下，增加启动项，重启后选择新增加的启动项。观察串口输出，可看到如下图所示信息：

                                        图16 虚拟机启动界面

seL4官方提供了一个性能测试工具sel4bench，直接编译运行就可以得到测试结果。我们仔细研究了sel4bench，然后花时间将每个测试用例移植到了Linux平台下，从而得出了Linux环境下的测试结果。

seL4内核版本: 11.0.0-dev

Linux发行版本CentOS Linux release 8.2.2004 (Core),Linux内核版本4.18.0-193.19.1.el8_2.x86_64

seL4微内核环境：使用seL4官方提供的测试工具sel4bench

Linux环境：将seL4官方提供的测试工具sel4bench移植到Linux内核环境

最小时间

平均时间

最大时间

Sel4

Linux

Sel4

linux

Sel4

linux

ipc

128

2102

131

2282

134

3121

irquser

113869

15605

380496

22724

646754

48663

scheduler

340

519

354

628

672

849

signal

187

5

214

48

337

126

fault

279

1718

284

1734

291

1754

hardware

167

58

180

205

390

7718

sync

1763

1752

1778

1966

1836

2181

表1 seL4与Linux性能测试结果

                                         图17 seL4与Linux性能对比测试

通过以上对比测试，可以看出seL4内核与Linux内核综合性能持平。

d)测试基准单位

TSC（Time Stamp Counter）时间戳计数器的值：从pentium开始，很多80x86微处理器都引入TSC，一个用于时间戳计数器的64位的寄存器，它在每个时钟信号到来时加一。当前使用的CPU主频为2.90GHz（2903.998MHz）,所以计数器的单位大约是0.34ns

e)测试原理：

seL4微内核和Linux内核之间主要做了以下对比测试：

ipc Benchmarks：进程间通信机制( Inter-Process Communication,IPC)是一项影响内核操作系统整体性能的关键因素。为了评估IPC通信的实时性能, ipc Benchmarks测试用例中通过统计内核IPC通信机制下消息在内核中的时间消耗，用以测试高实时优先级进程的通信延时。

irquser Benchmarks：中断处理是整个系统中优先级最高的代码，在系统运行过程中，中断程序可以抢占到任意任务级别的代码运行，而且中断也分等级，高级别中断抢占低级别中断。系统实时性是依靠中断机制来保证的，多任务的环境运行基础也是中断机制。所以对于衡量内核性能，最重要的指标就是中断延迟。irquser Benchmarks测试用例用来测试内核的中断延迟。

scheduler Benchmarks：主要用于统计任务切换时间(task switching time)，即系统在两个独立的、处于就绪态并且具有相同或不同优先级的任务之间切换所需要的时间。切换所需的时间主要取决于保存任务上下文所用的数据结构以及操作系统采用的调度算法的效率。产生任务切换的原因可以是资源可得，信号量的获取等。任务切换过程增加了应用程序的额外负荷。CPU的内部寄存器越多，额外负荷就越重。任务切换所需要的时间取决于CPU有多少寄存器要入栈。

signal Benchmarks：信号量混洗时间是指从一个任务释放信号量到另一个等待该信号量的任务被激活的时间延迟。在操作系统中，通常有许多任务同时竞争某一共享资源，基于信号量的互斥访问保证了任一时刻只有一个任务能够访问公共资源。信号量混洗时间反映了与互斥有关的时间开销，因此也是衡量内核实时性能的一个重要指标。

fault Benchmarks：异常是可以打断CPU正在运行流程的一些事情，比如外部中断、未定义指令、试图修改只读数据、执行swi指令(中断指令)等。当这些事情发生时，CPU暂停当前的程序,先处理异常事件,然后再继续执行被中断的程序。中断也是异常的一种。fault Benchmarks测试用例用于统计内核处理异常时间消耗。

hardware Benchmarks：用于统计内核执行空系统调用的时间消耗。

sync Benchmarks：互斥锁是使用简单的加锁的方法来控制对共享资源的存取。互斥锁只有两种状态，也就是上锁和解锁。可以把互斥锁看作某种意义上的全局变量。在同一时刻只能有一个线程掌握某个互斥上的锁，拥有上锁状态的线程能够对共享资源进行操作。若其他线程希望上锁一个已经上锁了的互斥锁，则该线程就会挂起，直到上锁的线程释放掉互斥锁为止。互斥锁使得共享资源按序在各个线程中操作。sync Benchmarks使用互斥锁和信号量实现多线程间的同步，统计同步信号发出到所有等待线程接收到同步信号的时间消耗。